$\forall$${\it es}$:ES, ${\it Fail}$:AbsInterface(Top), $A$:Type, $X$:AbsInterface($A$), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ alive($X$))) $\Leftarrow\!\Rightarrow$ (($\uparrow$($e$ $\in_{b}$ $X$)) \& ($\neg$($\exists$${\it e'}$:E. ((${\it e'}$ $<$loc $e$) \& ($\uparrow$(${\it e'}$ $\in_{b}$ ${\it Fail}$))))))